| Definitions |  x:A. B(x), P   Q, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val), P & Q, t  T, let x,y,z = a in t(x;y;z),  ,  A,  b, vartype(i;x), islocal(k), A & B, isl(x), act(k), valtype(i;a), outl(x), Msg(M), 1of(t), 2of(t), kindcase(k; a.f(a); l,t.g(l;t) ), Prop, A B, False,   x. t(x), x,y. t(x;y), S  T, S  T, outr(x), if b t else f fi, lnk(k), tag(k), b, true, false, time(e), loc(e), P  Q, P Q,  T, True, V(i;k), kind(e), act(e), val(e), FairFifo, w-machine-constraint(w), w-automaton(T;TA;M), Knd, x(s), x(s1,s2), E, SQType(T), {T}, isrcv(k), rcv(l,tg), w.TA, locl(a) |
| Lemmas | assert wf, islocal wf, kind wf, w-info wf, w-E wf, isrcv wf, fair-fifo wf, world wf, loc wf, Id wf, w-machine wf, w-automaton wf, w-T wf, w-TA wf, w-M wf, nat wf, not wf, w-isnull wf, w-a wf, w-vartype wf, w-s wf, le wf, w-kind wf, w-val wf, subtype rel self, kindcase wf, IdLnk wf, isl wf, actof wf, unit wf, w-valtype wf, outl wf, Knd wf, false wf, true wf, Msg wf, w-m wf, lsrc wf, mlnk wf, w-loc-lemma, pi1 wf, pi2 wf, squash wf, bool wf, w-state-when, w-loc wf, Id sq, w-eval wf, w-kind-lemma, w-time wf, rcv?-kind, sender wf |
